T:Type, f:(TT). retraction(T;f)  (x:T. y:T. (f(y) = y & y is f*(x))) 

latex

Definitions

Type, x:AB(x), t  T, {x:A| B(x)} , , |g|, S  T, A  B, , Void, False, A, x:A  B(x), left + right, P  Q, n - m, retraction(T;f), i  j , -n, #$n, f(a), n+m, y is f*(x), s = t, P & Q, x:A. B(x), a < b, P  Q, x:A. B(x), , hd(l), y=f*(x) via L, , type List, <a, b>, A c B, [car / cdr], [], A List, last(L), , Unit, (xL.P(x)), xL. P(x), |r|, x f y, a < b, a <p b, a  b, |p|, a ~ b, b | a, x,y:A//B(x;y), b, Atom, Dec(P), i  j < k, s ~ t, SQType(T), {T}, tl(l), i z j, i <z j, l[i], {i..j}

Lemmas

not wf, guard wf, decidable int equal, false wf, int seg wf, fun-connected transitivity, fun-connected weakening eq, fun-path wf, ge wf, nat properties, nat ind tp, fun-connected wf, member wf, le wf, nat wf